COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	\\M1BASL30\M2BASB30\M3NGR25\M4NGR20\F2\CSTANFORD UNIVERSITY
C00005 ENDMK
C⊗;
\\M1BASL30;\M2BASB30;\M3NGR25;\M4NGR20;\F2\CSTANFORD UNIVERSITY
\F3\CSTANFORD, CALIFORNIA 94305
\F4COMPUTER SCIENCE DEPARTMENT\←L\-R\/'7;\+R\→.\→S   Telephone:
\←S\→.415-497-4971
\F1\CJUl 23, 1974




Dear Mr Schorer:

\JDon't give up; I still do exist. The problem is to get manuscript finished
as soon as possible. I'm glad you are getting some good from text, though
the version you have is very much outdated. In particular large revisions
to incorporate Scott's semantics as applied to LISP have been incorporated.
By the way I would like to know where your copy came from; they copies
seem to by multiplying. 

On fixed-points: they are basically solutions to (functional) equations.
Think of fact <= λ[x][x=0; T → x*fact[x-1]] as an equation in fact. A
solution (i.e. fixed point) is a function. There are good reasons why
you should think of <= in this fashion. Book will explain why.

As to proving assem. prog.: I think it is a step in to wrong direction.
Being able to SPECIFY without PROGRAM is more useful and probably more
feasible. There are too many difficulties in proving properties
of assemb. progs. since they have almost no inherent structure; c.f.
argument against goto's. It applys "in spades" to assembly language.
\.
\←L\→S\←R\-L\/'2;\+L\→L

Yours sincerely,



John R. Allen
Research Associate
Computer Science Dept
Artificial Intelligence Labs

\←S\→L